package org.stragma.apply.modules

import org.kiama.rewriting._
import org.kiama.rewriting.Rewriter.{attempt,rulefs,Strategy,Term,topdown}

import org.stragma.apply.signatures.Apply._
import org.stragma.apply.signatures.Options._
import org.stragma.apply.signatures.Conversions._
import org.stragma.apply.modules.Options._
import org.stragma.apply.util._

import org.stragma.util.Configuration._

/*
 * Add assertions that can be derived from the code so that further 
 * simplifications can be performed.
 * Note that the assertions are themselves simplified before use, so it should be possible to
 * use them correctly to derive what we need even if they contain || (or) expressions
 * provided that one of the || branches resolves to true.
 */
object Addassertions extends TermInputOutput {
	
	/**
	 * Port of add-assertions strategy
	 */
	def add_assertions : Strategy = topdown( attempt( IfAssertion <+ ForAssertion ) ) 
	
	/*  This part of the code in Apply has been commented out, this is the original add_assertions code
		{
		// topdown(attempt(get_option(Generate_if_assertions()) <+ IfAssertion <+ 
		// get_option(Generate_loop_assertions) <* ForAssertion))
		if (get_option(Generate_if_assertions()).isDefined) {
			if (get_option(Generate_loop_assertions()).isDefined) {
				//topdown(attempt(IfAssertion <+ get_option(Generate_loop_assertions()) <* ForAssertion))
				topdown(attempt(IfAssertion <+ ForAssertion))
			} else {
				topdown(attempt(IfAssertion))
			}
		}
	}*/

	/*
	 * Port of strategy from Addassertions
	 */
	def remove_duplicate_assertions = topdown( attempt( RemoveDuplicateAssertion ) )

	/*
	 * Port of the IfAssertion rules
	 */
	def IfAssertion = 
		rulefs {
			// IfAssertion : |[ if e then s endif; ]| -> |[ if e then assert e; s endif; ]|
			// IfAssertion : |[ if e then s1 else s2 endif; ]| -> |[ if e then assert e; s1 else s2 endif; ]|
			case If( e, s ) 
				=> If( e, 
					Statements( Assert(e) ::: s ) )
				case IfElse( e, s1 , s2 )
				=> IfElse(e,
					Statements( Assert(e) ::: s1 ),
					Statements( Assert(Not(e)) ::: s2 ))
		}
	
	/*
	 * Port of the ForAssertion rule
	 */
	def ForAssertion = rulefs {
		// For(v,e1,e2,s) -> For(v,e1,e2,Statements([Assert( |[ ~v >= ~e1 and ~v <= ~e2 ]| ),s]))
		case For ( v, e1, e2, s )	
			=> For( v,e1,e2,
				Statements((Assert(Geq(v,e1) and Leq(v,e2)) ::: 
				s)))
		}
	
	/*
	 * Removes duplicate assertions
	 */
	def RemoveDuplicateAssertion = rulefs {
		// Unlike in Apply this version does not support nested statement
		// RemoveDuplicateAssertion : Statements([Assert(e),Statements([Assert(e),s])]) ->
		// 			Statements([Assert(e),s])
		case Statements(Assert(e) :: Assert(e1) :: s)
			if (e==e1) => 
				Statements(Assert(e) :: s)
	}
	
	/*
	 * Helper method to invoke function from Java
	 */
	def add_assertionsHelper(term : Term) : Term = {
		set_config ( ( Generate_if_assertions(),true ) )
		set_config ( ( Generate_loop_assertions(),true ) )
		(add_assertions(term)).get
	}
	
	/*
	 * This helper method executes add_assertions n times and returns
	 * the very last result the caller
	 */
	def add_assertionsHelper(term : Term, n : scala.Int) : Term = {
		var result : Term = scala.None
		for(i <- 0 until n) {
			result = (add_assertions(term)).get
			
			// Added the println to mimic the way strategoxt.jar works
			println(result)
		}
		
		result
	}
	
	/*
	 * This helper method executes add_assertions n times and returns
	 * the very last result to the caller
	 */
	def add_assertionsHelper(file : String, n : scala.Int) : Term = {
		set_config ( ( Generate_if_assertions(),true ) )
		set_config ( ( Generate_loop_assertions(),true ) )
		val iTerm = loadTermFromFile(file)
		add_assertionsHelper(iTerm, n)
	}
}